T:Type, R:(TT).
SWellFounded(R(x,y))  (x, y:T. Dec(z:T. (R(x,z) & R(z,y))))  R^+ => R!^+ 

latex

Definitions	{x:A| B(x)} , t  T, x:AB(x), x:A  B(x), Type, , False, A, A  B, , x f y, R1 => R2, R^+, SWellFounded(R(x;y)), P & Q, Dec(P), R!, rel_exp(T;R;n), f(a), , x:A. B(x), P  Q, x:A. B(x), #$n, a < b, , {T}, SQType(T), s = t, s ~ t, left + right, P  Q, b, , P  Q, i  j , -n, n+m, n - m, Void, (i = j)
Lemmas	rel exp add, rel-immediate wf, le wf, nat wf, ge wf, nat properties, bool cases, eqtt to assert, bool sq, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, decidable int equal, nat plus wf, rel exp wf, nat plus inc